Hierarchical Combination of Intruder Theories
Identifieur interne : 005471 ( Main/Exploration ); précédent : 005470; suivant : 005472Hierarchical Combination of Intruder Theories
Auteurs : Yannick Chevalier [France] ; Michaël Rusinowitch [France]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
Abstract: Recently automated deduction tools have proved to be very effective for detecting attacks on cryptographic protocols. These analysis can be improved, for finding more subtle weaknesses, by a more accurate modelling of operators employed by protocols. Several works have shown how to handle a single algebraic operator (associated with a fixed intruder theory) or how to combine several operators satisfying disjoint theories. However several interesting equational theories, such as exponentiation with an abelian group law for exponents remain out of the scope of these techniques. This has motivated us to introduce a new notion of hierarchical combination for intruder theories and to show decidability results for the deduction problem in these theories. Under a simple hypothesis, we were able to simplify this deduction problem. This simplification is then applied to prove the decidability of constraint systems w.r.t. an intruder relying on exponentiation theory.
Url:
DOI: 10.1007/11805618_9
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 002932
- to stream Istex, to step Curation: 002897
- to stream Istex, to step Checkpoint: 001324
- to stream Main, to step Merge: 005617
- to stream PascalFrancis, to step Corpus: 000390
- to stream PascalFrancis, to step Curation: 000643
- to stream PascalFrancis, to step Checkpoint: 000378
- to stream Main, to step Merge: 005783
- to stream Main, to step Curation: 005471
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Hierarchical Combination of Intruder Theories</title><author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:AE07493556FEBFBC753E05070A80B8E44E84C788</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/11805618_9</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-73WNMMNW-G/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">002932</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">002932</idno><idno type="wicri:Area/Istex/Curation">002897</idno><idno type="wicri:Area/Istex/Checkpoint">001324</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001324</idno><idno type="wicri:doubleKey">0302-9743:2006:Chevalier Y:hierarchical:combination:of</idno><idno type="wicri:Area/Main/Merge">005617</idno><idno type="wicri:source">INIST</idno><idno type="RBID">Pascal:07-0517948</idno><idno type="wicri:Area/PascalFrancis/Corpus">000390</idno><idno type="wicri:Area/PascalFrancis/Curation">000643</idno><idno type="wicri:Area/PascalFrancis/Checkpoint">000378</idno><idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000378</idno><idno type="wicri:doubleKey">0302-9743:2006:Chevalier Y:hierarchical:combination:of</idno><idno type="wicri:Area/Main/Merge">005783</idno><idno type="wicri:Area/Main/Curation">005471</idno><idno type="wicri:Area/Main/Exploration">005471</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Hierarchical Combination of Intruder Theories</title><author><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>IRIT Université Paul Sabatier</wicri:regionArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation wicri:level="1"><country xml:lang="fr">France</country><wicri:regionArea>LORIA-INRIA-Lorraine</wicri:regionArea></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Abelian group</term><term>Automatic proving</term><term>Cryptanalysis</term><term>Decidability</term><term>Equational theory</term><term>Exponentiation</term><term>Intruder</term><term>Modeling</term><term>Rewriting</term></keywords><keywords scheme="Pascal" xml:lang="fr"><term>Cryptanalyse</term><term>Décidabilité</term><term>Démonstration automatique</term><term>Exponentiation</term><term>Groupe abélien</term><term>Intrus</term><term>Modélisation</term><term>Réécriture</term><term>Théorie équationnelle</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: Recently automated deduction tools have proved to be very effective for detecting attacks on cryptographic protocols. These analysis can be improved, for finding more subtle weaknesses, by a more accurate modelling of operators employed by protocols. Several works have shown how to handle a single algebraic operator (associated with a fixed intruder theory) or how to combine several operators satisfying disjoint theories. However several interesting equational theories, such as exponentiation with an abelian group law for exponents remain out of the scope of these techniques. This has motivated us to introduce a new notion of hierarchical combination for intruder theories and to show decidability results for the deduction problem in these theories. Under a simple hypothesis, we were able to simplify this deduction problem. This simplification is then applied to prove the decidability of constraint systems w.r.t. an intruder relying on exponentiation theory.</div></front></TEI><affiliations><list><country><li>France</li></country></list><tree><country name="France"><noRegion><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name></noRegion><name sortKey="Chevalier, Yannick" sort="Chevalier, Yannick" uniqKey="Chevalier Y" first="Yannick" last="Chevalier">Yannick Chevalier</name><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 005471 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 005471 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:AE07493556FEBFBC753E05070A80B8E44E84C788
|texte= Hierarchical Combination of Intruder Theories
}}
| This area was generated with Dilib version V0.6.33. |  |